Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(append,nil),ys)  → ys
2:    app(app(append,app(app(cons,x),xs)),ys)  → app(app(cons,x),app(app(append,xs),ys))
3:    app(app(flatwith,f),app(leaf,x))  → app(app(cons,app(f,x)),nil)
4:    app(app(flatwith,f),app(node,xs))  → app(app(flatwithsub,f),xs)
5:    app(app(flatwithsub,f),nil)  → nil
6:    app(app(flatwithsub,f),app(app(cons,x),xs))  → app(app(append,app(app(flatwith,f),x)),app(app(flatwithsub,f),xs))
There are 13 dependency pairs:
7:    APP(app(append,app(app(cons,x),xs)),ys)  → APP(app(cons,x),app(app(append,xs),ys))
8:    APP(app(append,app(app(cons,x),xs)),ys)  → APP(app(append,xs),ys)
9:    APP(app(append,app(app(cons,x),xs)),ys)  → APP(append,xs)
10:    APP(app(flatwith,f),app(leaf,x))  → APP(app(cons,app(f,x)),nil)
11:    APP(app(flatwith,f),app(leaf,x))  → APP(cons,app(f,x))
12:    APP(app(flatwith,f),app(leaf,x))  → APP(f,x)
13:    APP(app(flatwith,f),app(node,xs))  → APP(app(flatwithsub,f),xs)
14:    APP(app(flatwith,f),app(node,xs))  → APP(flatwithsub,f)
15:    APP(app(flatwithsub,f),app(app(cons,x),xs))  → APP(app(append,app(app(flatwith,f),x)),app(app(flatwithsub,f),xs))
16:    APP(app(flatwithsub,f),app(app(cons,x),xs))  → APP(append,app(app(flatwith,f),x))
17:    APP(app(flatwithsub,f),app(app(cons,x),xs))  → APP(app(flatwith,f),x)
18:    APP(app(flatwithsub,f),app(app(cons,x),xs))  → APP(flatwith,f)
19:    APP(app(flatwithsub,f),app(app(cons,x),xs))  → APP(app(flatwithsub,f),xs)
The approximated dependency graph contains one SCC: {8,10,12,13,15,17,19}.
Tyrolean Termination Tool  (0.18 seconds)   ---  May 3, 2006